r,s:rationals. qeq(r; s)   

latex

Definitions	P  Q, P  Q, P  Q, prop{i:l}, P  Q, t  T, x:A. B(x), trans(T; x,y.E(x;y)), sym(T; x,y.E(x;y)), equiv_rel(T; x,y.E(x;y)), False, A, Unit, , rationals, ff, , tt
Lemmas	qeq-equiv, bfalse wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, rationals wf, btrue wf, qeq wf, bool wf